w_locle(w;x;y) == x ((x,y. ((first(y))) c (x = pred(y)))^*) y 

latex

---

clarification:

w_locle(w;x;y)
== x 
== rel_star(w-E(w);(x,y. ((first(e.w-pred(w;e);y)))
== c (x = pred(e.w-pred(w;e);y)  w-E(w)))) y 

latex

Definitions	x f y, R^*, A c B, A, b, first(e), s = t, E, pred(e), x.A(x), w-pred(w;e)
FDL editor aliases	w_locle